Inference at * 1 1 
Iof proof for Lemma uni sat imp in uni set:



1. T : Type
2. a : T
3. Q : T
4. Q(a)
5. a':T. Q(a')  (a' = a)
6. y : T
7. Q(y)
  y = a 

latex

 by ((BHyp 5) 
CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 4:n
C)) (first_tok :t) inil_term))) 

latex

C.

Definitions

t  T, P  Q, x:A. B(x)